(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
rpm_t_m_2#1(f_p(snd, x(x2)), x3) → Leaf(snd#2(x#1(x2, bot[2]), bot[3]))
rpm_t_m_9#1(fst, P(rpm_t_m_9(x4, x6, x8), x2), x5, x3) → Node(rpm_t_m_9#1(x4, x6, x8, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_9#1(fst, P(rpm_t_m_2(x4), x2), x5, x3) → Node(rpm_t_m_2#1(x4, bot[5]), fst#2(x5, bot[6]))
rpm_t_m_8#1(x3, x2, x1) → P(rpm_t_m_9(fst, x3, x2), rpm_t_m_10(x3, x2))
rpm#3(Leaf(x8), f_p(x12, x16), x4) → P(rpm_t_m_2(f_p(x12, x16)), rpm_t_m_3(x8))
rpm#3(Node(x8, x6), f_p(x2, x4), x10) → rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)
cond_fst_p#1(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
cond_fst_p#1(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_9(x2, x3, x4), x1), x5) → rpm_t_m_9#1(x2, x3, x4, x5)
fst#2(P(rpm_t_m_2(x2), x1), x3) → rpm_t_m_2#1(x2, x3)
snd#2(P(x18, rpm_t_m_3(x14)), x18) → x14
snd#2(P(x2, rpm_t_m_10(x6, x4)), x2) → min#2(snd#2(x6, bot[7]), snd#2(x4, bot[8]))
min#2(0, x12) → 0
min#2(S(x16), 0) → 0
min#2(S(x4), S(x2)) → S(min#2(x4, x2))
x#1(f(x4), x3) → rpm#3(x4, f_p(snd, x(f(x4))), bot[11])
main(x1) → cond_fst_p#1(x#1(f(x1), bot[0]), bot[1])
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
rpm#3(Node(x8, x6), f_p(x2, x4), x10) →+ rpm_t_m_8#1(rpm#3(x8, f_p(x2, x4), bot[9]), rpm#3(x6, f_p(x2, x4), bot[10]), x10)
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x8 / Node(x8, x6)].
The result substitution is [x10 / bot[9]].
(2) BOUNDS(n^1, INF)